<html xmlns:v="urn:schemas-microsoft-com:vml"
xmlns:o="urn:schemas-microsoft-com:office:office"
xmlns:w="urn:schemas-microsoft-com:office:word"
xmlns="http://www.w3.org/TR/REC-html40">

<head>
<meta http-equiv=Content-Type content="text/html; charset=iso-8859-1">
<meta name=ProgId content=Word.Document>
<meta name=Generator content="Microsoft Word 9">
<meta name=Originator content="Microsoft Word 9">
<link rel=File-List href="./AppendixE_files/filelist.xml">
<link rel=Edit-Time-Data href="./AppendixE_files/editdata.mso">
<!--[if !mso]>
<style>
v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style>
<![endif]-->
<title>Appendix E </title>
<style>
<!--
 /* Font Definitions */
@font-face
	{font-family:Tahoma;
	panose-1:2 11 6 4 3 5 4 4 2 4;
	mso-font-charset:0;
	mso-generic-font-family:swiss;
	mso-font-pitch:variable;
	mso-font-signature:1627421319 -2147483648 8 0 66047 0;}
@font-face
	{font-family:"Microsoft Sans Serif";
	panose-1:2 11 6 4 2 2 2 2 2 4;
	mso-font-charset:0;
	mso-generic-font-family:swiss;
	mso-font-pitch:variable;
	mso-font-signature:1627421663 -2147483648 8 0 66047 0;}
@font-face
	{font-family:BrushScrD;
	panose-1:3 0 0 0 0 0 0 0 0 0;
	mso-font-charset:0;
	mso-generic-font-family:script;
	mso-font-pitch:variable;
	mso-font-signature:-2147483473 30971 0 0 147 0;}
@font-face
	{font-family:"Signet Roundhand";
	mso-font-alt:"Courier New";
	mso-font-charset:0;
	mso-generic-font-family:script;
	mso-font-pitch:variable;
	mso-font-signature:7 0 0 0 19 0;}
 /* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
	{mso-style-parent:"";
	margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:windowtext;}
h1
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:1;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-font-kerning:0pt;
	mso-ansi-language:EN-GB;
	font-weight:normal;
	text-decoration:underline;
	text-underline:single;}
h2
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:center;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:2;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:normal;
	font-style:italic;
	mso-bidi-font-style:normal;}
h3
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:3;
	font-size:14.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:normal;}
h4
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:4;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:bold;
	mso-bidi-font-weight:normal;
	text-decoration:underline;
	text-underline:single;}
h5
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:5;
	font-size:14.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:bold;
	mso-bidi-font-weight:normal;
	text-decoration:underline;
	text-underline:single;}
h6
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	text-indent:.5in;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:6;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:normal;
	font-style:italic;
	mso-bidi-font-style:normal;}
p.MsoHeading7, li.MsoHeading7, div.MsoHeading7
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:7;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-style:italic;
	mso-bidi-font-style:normal;}
p.MsoHeading8, li.MsoHeading8, div.MsoHeading8
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:8;
	font-size:14.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	text-decoration:underline;
	text-underline:single;}
p.MsoHeading9, li.MsoHeading9, div.MsoHeading9
	{mso-style-next:Normal;
	margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:center;
	mso-pagination:widow-orphan;
	page-break-after:avoid;
	mso-outline-level:9;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;
	font-weight:bold;
	mso-bidi-font-weight:normal;}
p.MsoIndex1, li.MsoIndex1, div.MsoIndex1
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:11.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex2, li.MsoIndex2, div.MsoIndex2
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:22.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex3, li.MsoIndex3, div.MsoIndex3
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:33.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex4, li.MsoIndex4, div.MsoIndex4
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:44.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex5, li.MsoIndex5, div.MsoIndex5
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:55.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex6, li.MsoIndex6, div.MsoIndex6
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:66.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex7, li.MsoIndex7, div.MsoIndex7
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:77.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex8, li.MsoIndex8, div.MsoIndex8
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:88.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndex9, li.MsoIndex9, div.MsoIndex9
	{mso-style-update:auto;
	mso-style-next:Normal;
	margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:99.0pt;
	margin-bottom:.0001pt;
	text-indent:-11.0pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoFootnoteText, li.MsoFootnoteText, div.MsoFootnoteText
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoHeader, li.MsoHeader, div.MsoHeader
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	tab-stops:center 207.65pt right 415.3pt;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoFooter, li.MsoFooter, div.MsoFooter
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	tab-stops:center 207.65pt right 415.3pt;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoIndexHeading, li.MsoIndexHeading, div.MsoIndexHeading
	{mso-style-next:"Index 1";
	margin-top:12.0pt;
	margin-right:0in;
	margin-bottom:6.0pt;
	margin-left:0in;
	text-align:center;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:15.5pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	font-weight:bold;}
span.MsoFootnoteReference
	{vertical-align:super;}
span.MsoEndnoteReference
	{vertical-align:super;}
p.MsoEndnoteText, li.MsoEndnoteText, div.MsoEndnoteText
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoTitle, li.MsoTitle, div.MsoTitle
	{margin:0in;
	margin-bottom:.0001pt;
	text-align:center;
	mso-pagination:widow-orphan;
	font-size:12.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:windowtext;
	font-weight:bold;
	mso-bidi-font-weight:normal;}
p.MsoBodyText, li.MsoBodyText, div.MsoBodyText
	{margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyTextIndent, li.MsoBodyTextIndent, div.MsoBodyTextIndent
	{margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:13.5pt;
	margin-bottom:.0001pt;
	text-align:justify;
	text-indent:.65pt;
	mso-pagination:widow-orphan;
	mso-layout-grid-align:none;
	text-autospace:none;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyText2, li.MsoBodyText2, div.MsoBodyText2
	{margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	border:none;
	mso-border-top-alt:solid windowtext 1.5pt;
	mso-border-bottom-alt:solid windowtext 1.5pt;
	padding:0in;
	mso-padding-alt:1.0pt 0in 1.0pt 0in;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyText3, li.MsoBodyText3, div.MsoBodyText3
	{margin:0in;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyTextIndent2, li.MsoBodyTextIndent2, div.MsoBodyTextIndent2
	{margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:13.5pt;
	margin-bottom:.0001pt;
	text-align:justify;
	mso-pagination:widow-orphan;
	mso-layout-grid-align:none;
	text-autospace:none;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;
	mso-ansi-language:EN-GB;}
p.MsoBodyTextIndent3, li.MsoBodyTextIndent3, div.MsoBodyTextIndent3
	{margin-top:0in;
	margin-right:0in;
	margin-bottom:0in;
	margin-left:.5in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:9.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
p.MsoBlockText, li.MsoBlockText, div.MsoBlockText
	{margin-top:0in;
	margin-right:-.35pt;
	margin-bottom:0in;
	margin-left:3.5in;
	margin-bottom:.0001pt;
	text-align:justify;
	text-indent:-3.5in;
	mso-pagination:widow-orphan;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
a:link, span.MsoHyperlink
	{mso-style-parent:"";
	color:blue;
	text-decoration:underline;
	text-underline:single;}
a:visited, span.MsoHyperlinkFollowed
	{color:purple;
	text-decoration:underline;
	text-underline:single;}
strong
	{mso-bidi-font-weight:normal;}
em
	{mso-bidi-font-style:normal;}
p.MsoDocumentMap, li.MsoDocumentMap, div.MsoDocumentMap
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	background:navy;
	font-size:11.0pt;
	mso-bidi-font-size:10.0pt;
	font-family:Tahoma;
	mso-fareast-font-family:"Times New Roman";
	mso-bidi-font-family:"Times New Roman";
	color:black;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
	{margin:0in;
	margin-bottom:.0001pt;
	mso-pagination:widow-orphan;
	font-size:10.0pt;
	font-family:"Courier New";
	mso-fareast-font-family:"Times New Roman";
	mso-bidi-font-family:"Times New Roman";
	color:windowtext;
	mso-ansi-language:EN-GB;}
p
	{margin-right:0in;
	mso-margin-top-alt:auto;
	mso-margin-bottom-alt:auto;
	margin-left:0in;
	mso-pagination:widow-orphan;
	font-size:12.0pt;
	font-family:"Times New Roman";
	mso-fareast-font-family:"Times New Roman";
	color:black;}
span.Typewriter
	{mso-style-name:Typewriter;
	mso-style-parent:"";
	mso-ansi-font-size:10.0pt;
	mso-ascii-font-family:"Courier New";
	mso-hansi-font-family:"Courier New";}
span.l
	{mso-style-name:l;}
@page Section1
	{size:8.5in 11.0in;
	margin:1.0in 1.25in 1.0in 1.25in;
	mso-header-margin:.5in;
	mso-footer-margin:.5in;
	mso-paper-source:0;}
div.Section1
	{page:Section1;}
 /* List Definitions */
@list l0
	{mso-list-id:159926975;
	mso-list-type:simple;
	mso-list-template-ids:134807577;}
@list l0:level1
	{mso-level-number-format:alpha-lower;
	mso-level-text:"\(%1\)";
	mso-level-tab-stop:.25in;
	mso-level-number-position:left;
	margin-left:.25in;
	text-indent:-.25in;}
@list l1
	{mso-list-id:631440919;
	mso-list-type:hybrid;
	mso-list-template-ids:-1301522294 67698703 67698713 67698715 67698703 67698713 67698715 67698703 67698713 67698715;}
ol
	{margin-bottom:0in;}
ul
	{margin-bottom:0in;}
-->
</style>
<!--[if gte mso 9]><xml>
 <o:shapedefaults v:ext="edit" spidmax="1027"/>
</xml><![endif]--><!--[if gte mso 9]><xml>
 <o:shapelayout v:ext="edit">
  <o:idmap v:ext="edit" data="1"/>
 </o:shapelayout></xml><![endif]--><!--[if gte mso 9]><xml>
 <u1:DocumentProperties>
  <u1:Author> </u1:Author>
  <u1:Template>Normal</u1:Template>
  <u1:LastAuthor> </u1:LastAuthor>
  <u1:Revision>3</u1:Revision>
  <u1:TotalTime>1</u1:TotalTime>
  <u1:Created>2005-01-15T18:29:00Z</u1:Created>
  <u1:LastSaved>2005-01-15T18:30:00Z</u1:LastSaved>
  <u1:Pages>3</u1:Pages>
  <u1:Words>1751</u1:Words>
  <u1:Characters>9983</u1:Characters>
  <u1:Company> </u1:Company>
  <u1:Lines>83</u1:Lines>
  <u1:Paragraphs>19</u1:Paragraphs>
  <u1:CharactersWithSpaces>12259</u1:CharactersWithSpaces>
  <u1:Version>9.2720</u1:Version>
 </u1:DocumentProperties>
</xml><![endif]--><!--[if gte mso 9]><xml>
 <u2:WordDocument>
  <u2:DisplayHorizontalDrawingGridEvery>0</u2:DisplayHorizontalDrawingGridEvery>
  <u2:DisplayVerticalDrawingGridEvery>0</u2:DisplayVerticalDrawingGridEvery>
  <u2:UseMarginsForDrawingGridOrigin/>
  <u2:Compatibility>
   <u2:FootnoteLayoutLikeWW8/>
   <u2:ShapeLayoutLikeWW8/>
   <u2:AlignTablesRowByRow/>
   <u2:ForgetLastTabAlignment/>
   <u2:LayoutRawTableWidth/>
   <u2:LayoutTableRowsApart/>
  </u2:Compatibility>
 </u2:WordDocument>
</xml><![endif]-->
</head>

<body bgcolor=silver lang=EN-US link=blue vlink=purple style='tab-interval:
.5in'>

<div class=Section1>

<div align=center>

<table border=0 cellpadding=0 width="80%" bgcolor=white style='width:80.0%;
 mso-cellspacing:1.5pt;background:white;mso-padding-alt:75.0pt 75.0pt 75.0pt 75.0pt'>
 <tr>
  <td width="100%" style='width:100.0%;padding:75.0pt 75.0pt 75.0pt 75.0pt'>
  <p class=MsoTitle align=left style='margin-left:1.0in;text-align:left'><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  font-weight:normal;mso-bidi-font-weight:bold'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>
  <div align=center>
  <table border=0 cellspacing=0 cellpadding=0 width=432 style='width:4.5in;
   border-collapse:collapse;border:none;mso-border-alt:solid windowtext .5pt;
   mso-padding-alt:0in 5.4pt 0in 5.4pt'>
   <tr>
    <td width=492 valign=top style='width:368.75pt;border:solid windowtext .5pt;
    padding:0in 5.4pt 0in 5.4pt'>
    <p class=MsoTitle align=left style='text-align:left'><span
    style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
    font-weight:normal;mso-bidi-font-weight:bold'><a href="QiPrograms.zip">Download
    Programs</a> <o:p></o:p></span></p>
    </td>
    <td width=492 valign=top style='width:368.75pt;border:solid windowtext .5pt;
    border-left:none;mso-border-left-alt:solid windowtext .5pt;padding:0in 5.4pt 0in 5.4pt'>
    <p class=MsoTitle align=left style='text-align:left'><span
    style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
    font-weight:normal;mso-bidi-font-weight:bold'><a href="contents.htm">Go to
    Contents Page</a><o:p></o:p></span></p>
    </td>
   </tr>
  </table>
  </div>
  <p class=MsoTitle align=left style='margin-left:1.0in;text-align:left'><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  font-weight:normal;mso-bidi-font-weight:bold'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>
  <p class=MsoTitle align=left style='margin-left:1.0in;text-align:left'><span
  style='font-size:14.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  font-weight:normal;mso-bidi-font-weight:bold'>Note that this HTML page was
  generated from Word 2000.<span style="mso-spacerun: yes">&nbsp; </span>Some
  of the code cannot be pasted into Qi. You are advised to download the program
  files through the above link.<o:p></o:p></span></p>
  <p class=MsoNormal align=center style='margin-top:0in;margin-right:-.35pt;
  margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt;text-align:center;
  mso-outline-level:1'><span lang=EN-GB style='font-size:18.0pt;mso-bidi-font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>
  <p class=MsoNormal align=center style='margin-top:0in;margin-right:-.35pt;
  margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt;text-align:center;
  mso-outline-level:1'><span lang=EN-GB style='font-size:18.0pt;mso-bidi-font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>Appendix E <u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-top:0in;margin-right:-.35pt;
  margin-bottom:0in;margin-left:.5in;margin-bottom:.0001pt;text-align:center'><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></p>
  <h3 align=center style='margin-left:.5in;text-align:center'><span lang=EN-GB
  style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>The Type Security of the </span><span
  lang=EN-GB style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:
  BrushScrD;mso-bidi-font-style:italic'>L</span><span lang=EN-GB
  style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-style:italic'> </span><span
  lang=EN-GB style='font-size:18.0pt;mso-bidi-font-size:10.0pt;font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Type System<u3:p></u3:p></span></h3>
  <h3 align=center style='margin-left:.5in;text-align:center'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></h3>
  <h3 style='margin-left:.5in'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>We
  define a <b>primitive data structure</b></span><!--[if supportFields]><b
  style='mso-bidi-font-weight:normal'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> XE &quot;<b style='mso-bidi-font-weight:normal'>primitive
  data structure</b>&quot; </span><![endif]--><!--[if supportFields]><b
  style='mso-bidi-font-weight:normal'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></b><![endif]--><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'><span style="mso-spacerun: yes">&nbsp;</span>(p.d.) as a
  symbol, boolean</span><!--[if supportFields]><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'><span style='mso-element:field-begin'></span> XE
  &quot;boolean&quot; </span><![endif]--><!--[if supportFields]><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>, number, string, character, or list
  or tuple of p.d.s. The expression &#8216;|- e : A&#8217; is taken to mean &#8216;e : A is
  provable in the </span><span lang=EN-GB style='font-size:11.0pt;mso-bidi-font-size:
  10.0pt;font-family:BrushScrD;mso-bidi-font-style:italic'>L </span><span
  lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>type system&#8217;. <span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></h3>
  <h3 style='margin-left:.5in'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></h3>
  <h3 style='margin-left:.5in'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Our
  proof of the correctness of the </span><span lang=EN-GB style='font-size:
  11.0pt;mso-bidi-font-size:10.0pt;font-family:BrushScrD;mso-bidi-font-style:
  italic'>L</span><span lang=EN-GB style='font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> type system is covered in 3
  theorems.<span style="mso-spacerun: yes">&nbsp; </span>In the first theorem,
  we demonstrate that if e is p.d. and |- e : A, then e : A.<span
  style="mso-spacerun: yes">&nbsp; </span>In the second theorem, we demonstrate
  the <b>subject reduction</b></span><!--[if supportFields]><b
  style='mso-bidi-font-weight:normal'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> XE &quot;<b style='mso-bidi-font-weight:normal'>subject
  reduction</b>&quot; </span><![endif]--><!--[if supportFields]><b
  style='mso-bidi-font-weight:normal'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></b><![endif]--><b
  style='mso-bidi-font-weight:normal'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-bidi-font-weight:bold'><span style="mso-spacerun:
  yes">&nbsp;</span>property</span></span></b><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>, namely;<u3:p></u3:p></span></h3>
  <h3 style='margin-left:.5in'><span lang=EN-GB style='font-size:10.0pt;
  font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></h3>
  <h3 align=center style='margin-left:.5in;text-align:center'><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>if |- e : A and e </span><span lang=EN-GB
  style='font-size:10.0pt;font-family:Symbol'>�</span><span lang=EN-GB
  style='font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> e* then |- e* : A.<u3:p></u3:p></span></h3>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>The
  third theorem is a consequence of both these theorems; namely that if |- e :
  A, then the evaluation of e to a p.d. e* will produce an expression of type
  A. <span style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Notice
  that it is not true that if e </span><span lang=EN-GB style='font-family:
  Symbol;mso-ansi-language:EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> e* and |- e* : A then |- e : A. The
  expression (if (= 1 0) a &#8220;a&#8221;) evaluates to &#8220;a&#8221;, but although |- &#8220;a&#8221; : string,
  it is not a theorem</span><!--[if supportFields]><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>theorem</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>that (if (= 1 0) a &#8220;a&#8221;) : string.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Theorem 1: if e is a p.d. and</span></b><!--[if supportFields]><b
  style='mso-bidi-font-weight:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span></span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  XE &quot;</span><b style='mso-bidi-font-weight:normal'><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>self-evaluating</span></b><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><b
  style='mso-bidi-font-weight:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></b><![endif]--><b
  style='mso-bidi-font-weight:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-bidi-font-weight:
  bold'><span style="mso-spacerun: yes">&nbsp;</span>|- e : A then e : A.<u3:p></u3:p></span></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Proof:</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style="mso-spacerun:
  yes">&nbsp; </span>Suppose e is a p.d. and |- e : A; then e is either <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.75in;text-align:justify;text-indent:
  -.25in;mso-list:l0 level1 lfo2;tab-stops:list .25in'><![if !supportLists]>(a)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(a)</span><span
  style='font-size:7.0pt'>&nbsp;&nbsp;&nbsp; </span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>a primitive
  expression (symbol, boolean</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>boolean</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  number, string or character), or<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.75in;text-align:justify;text-indent:
  -.25in;mso-list:l0 level1 lfo2;tab-stops:list .25in'><![if !supportLists]>(b)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(b)</span><span
  style='font-size:7.0pt'>&nbsp;&nbsp;&nbsp; </span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>a list of
  p.d.s,</span><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>list</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>or<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.75in;text-align:justify;text-indent:
  -.25in;mso-list:l0 level1 lfo2;tab-stops:list .25in'><![if !supportLists]>(c)<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp; </span><![endif]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(c)</span><span
  style='font-size:7.0pt'>&nbsp;&nbsp;&nbsp;&nbsp; </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>a
  tuple of p.d.s.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-layout-grid-align:
  none;text-autospace:none'><b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>Suppose (a)</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  then the type of e is determined by </span><span style='font-family:Symbol'>t,
  </span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>so that e : string iff string </span><span
  style='mso-bidi-font-size:12.0pt;font-family:Symbol'>�</span><span
  style='font-size:12.0pt;font-family:Symbol'> </span><span style='font-family:
  Symbol'>t</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(e) etc.<span style="mso-spacerun: yes">&nbsp; </span>The
  only type rule in </span><span lang=EN-GB style='font-family:BrushScrD;
  mso-ansi-language:EN-GB;mso-bidi-font-style:italic'>L </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>for
  proving the type of e is the <i>Primitive Rule</i> which establishes e : A
  only if<span style="mso-spacerun: yes">&nbsp; </span>A </span><span
  style='mso-bidi-font-size:12.0pt;font-family:Symbol'>�</span><span
  style='font-size:12.0pt;font-family:Symbol'> </span><span style='font-family:
  Symbol'>t</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(e).<span style="mso-spacerun: yes">&nbsp; </span>Hence if
  |- e : A then A </span><span style='mso-bidi-font-size:12.0pt;font-family:
  Symbol'>�</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> </span><span style='font-family:Symbol'>t</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(e)
  and so e : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Suppose
  (b)</span></b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>, then e is a list</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>list</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>and the proof proceeds by
  induction.<span style="mso-spacerun: yes">&nbsp; </span>Let the <b>ultimate
  length</b> (</span><span style='font-family:Symbol'>u</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>)
  be defined as follows. <span style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:Symbol'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:Symbol'>u</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(x) = 1 where x is a primitive object</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;primitive object&quot; \b </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>For
  any list</span><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>list</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>l, </span><span style='font-family:
  Symbol'>u</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(l) = </span><span style='font-family:Symbol'>S</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(</span><span
  style='font-family:Symbol'>u</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(i)) where i is an element in l.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Base Case:</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span><span style='font-family:
  Symbol'>u</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(e) = 0<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>then
  e = []; according to the <i>Primitive Rule</i>, which is the only applicable
  rule, |- e : </span><span style='font-family:Symbol'>&quot;</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>A
  (list</span><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>list</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>A).<span style="mso-spacerun:
  yes">&nbsp; </span>By the inhabitation rule for lists (chapter 10); <span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:Symbol'>&quot;</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>A(e : (list</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>list</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>A) </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB;layout-grid-mode:line'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  (</span><span style='font-family:Symbol'>&quot;</span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x<span
  style="mso-spacerun: yes">&nbsp; </span>element (x,e) </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB;layout-grid-mode:
  line'>�</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> x : A))<a style='mso-footnote-id:ftn1' href="#_ftn1"
  name="_ftnref1" title=""><span class=MsoFootnoteReference><span
  style='mso-special-character:footnote'><![if !supportFootnotes]>[1]<![endif]></span></span></a><span
  class=MsoFootnoteReference>[1]<u3:p></u3:p></span></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Since
  ~</span><span style='font-family:Symbol'>$</span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x element(x,e)
  then e : </span><span style='font-family:Symbol'>&quot;</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>A:
  (list</span><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>list</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>A).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Inductive
  Case:</span></i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> the theorem</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>theorem</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>holds for all list</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>list</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>s
  l where </span><span style='font-family:Symbol'>u</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(l)
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB;
  layout-grid-mode:line'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> n.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Let
  e = [X | Y] be a list</span><!--[if supportFields]><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>list</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>expression of ultimate length n +
  1.<span style="mso-spacerun: yes">&nbsp; </span>Then if e has a type under
  Qi, it has the type (list A) for some A and so |- e : (list A).<span
  style="mso-spacerun: yes">&nbsp; </span>This can only be established by the <i>Cons
  (right) Rule</i> and so |- X : A and |- Y : (list A).<span
  style="mso-spacerun: yes">&nbsp; </span>By the inductive hypothesis we
  conclude that X : A and Y : (list A).<span style="mso-spacerun: yes">&nbsp;
  </span>In which case [X | Y] : (list A) and so e : (list A).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Suppose (c)</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>, then e is a tuple (@p <i>x y</i>).<span
  style="mso-spacerun: yes">&nbsp; </span>Let the <b>tuple</b> <b>size</b> (</span><span
  style='font-family:Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>) be defined as follows. <span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(<i>x</i>) = 0 if <i>x</i> is not a
  tuple.<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(@p <i>x y</i>) = </span><span
  style='font-family:Symbol'>1 + s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(<i>x</i>) </span><span
  style='font-family:Symbol'>+ s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(<i>y</i>).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>The
  proof is by induction on the size of </span><span style='font-family:Symbol'>s</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(e).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Base Case:</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span><span style='font-family:
  Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(e) = 1<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Suppose
  |- e : A; then for some B, C, A = (B * C) and |- (@p <i>x y</i>) : (B *
  C).<span style="mso-spacerun: yes">&nbsp; </span>But if |- (@p <i>x y</i>) :
  (B * C) then |- <i>x</i> : A and |- <i>y</i> : B. But since </span><span
  style='font-family:Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(<i>x</i>) = </span><span
  style='font-family:Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(<i>y</i>) = 0, <i>x</i> and <i>y</i>
  are not tuples and are primitive, <i>x</i> : B and <i>y</i> : C.<span
  style="mso-spacerun: yes">&nbsp; </span>By the inhabitation rule for tuples:<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>((@p
  <i>x y</i>) : (B * C)) </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB;layout-grid-mode:line'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  ((<i>x</i> : B) &amp; (<i>y</i> : C))<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Since
  the RHS of this equivalence is true, then (@p <i>x y</i>) : (B * C) and so e
  : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></i></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Inductive Case:</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> the theorem</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>theorem</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>holds for all tuple</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>list</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>s
  t where </span><span style='font-family:Symbol'>s</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(t)
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB;
  layout-grid-mode:line'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> n. <span style="mso-spacerun:
  yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Suppose
  </span><span style='font-family:Symbol'>s</span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(e) = n + 1
  and |- e : A; then for some B, C, A = (B * C) and |- (@p <i>x y</i>) : (B *
  C).<span style="mso-spacerun: yes">&nbsp; </span>But if |- (@p <i>x y</i>) :
  (B * C) then |- <i>x</i> : A and |- <i>y</i> : B.<span style="mso-spacerun:
  yes">&nbsp; </span>Also </span><span style='font-family:Symbol'>s</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(x)
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB;
  layout-grid-mode:line'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> n and </span><span style='font-family:
  Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(y) </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB;layout-grid-mode:line'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  n and so by the inductive hypothesis, <i>x</i> : B and <i>y</i> : C. By the
  inhabitation rule for tuples:<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal align=center style='margin-left:.5in;text-align:center'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>((@p
  <i>x y</i>) : (B * C)) </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB;layout-grid-mode:line'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  ((<i>x</i> : B) &amp; (<i>y</i> : C))<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Since
  the RHS of this equivalence is true, then (@p <i>x y</i>) : (B * C) and so e
  : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Theorem 2: if |- e : A and e </span></b><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  e* then |- e* : A.<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>The
  proof proceeds by cases. The reduction of e to e* must be one of the rules
  #0-16 in the semantics</span><!--[if supportFields]><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>semantics</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>for </span><span style='font-family:
  BrushScrD;mso-bidi-font-style:italic'>L</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #1; then e = (= <i>x y</i>) and if |- e : A then by the <i>Equality Rule</i></span><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE
  &quot;Equality Rule&quot; \b </span><![endif]--><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>A = boolean</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>boolean</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp; </span>By rule #1, e* = true and by the <i>Primitive
  Rule</i> |- true : boolean.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #2; then e = (= <i>x y</i>) and if |- e : A then by the <i>Equality Rule</i></span><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE
  &quot;Equality Rule&quot; \b </span><![endif]--><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>A = boolean</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>boolean</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp; </span>By rule #2, e* = false and by the <i>Primitive
  Rule</i> |- false : boolean.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #3; then e = (= <i>x y</i>) and suppose |- e : A</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>boolean</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp; </span>By rule #3, e* = </span><span
  style='font-family:Symbol'>^</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> or e* = </span><b><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  and by the rules for error conditions, e</span><span style='font-family:Symbol'>
  *</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #4; then e = ((</span><span style='font-family:Symbol'>l </span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>p</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  <i>x</i>) <i>y</i>).<span style="mso-spacerun: yes">&nbsp; </span>Assume |- e
  : A, then by the <i>Applications Rule</i></span><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE &quot;<i
  style='mso-bidi-font-style:normal'>Applications Rule</i>&quot; \b </span><![endif]--><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>for some B<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:2.0in;text-align:justify;text-indent:
  .5in'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>|- (</span><span style='font-family:Symbol'>l </span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>p</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  <i>x</i>) : B </span><span style='font-family:Symbol'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:2.0in;text-align:justify;text-indent:
  .5in'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>|- <i>y</i> : B<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Either
  <i>match</i>(<i>p</i>, <i>y</i>) = </span><b><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  or <i>match</i>(<i>p</i>, <i>y</i>) </span><span style='font-family:Symbol'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><b><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp;&nbsp; </span>Assume <i>match</i>(<i>p</i>, <i>y</i>)
  = </span><b><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>, then e* =</span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'> � </span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>and
  |- e* : A (since |- </span><b><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> : (</span><span style='font-family:
  Symbol'>&quot;</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> A A)).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Assume
  <i>match</i>(<i>p</i>, <i>y</i>) </span><span style='font-family:Symbol'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><b><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  then either<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(a)
  <i>p</i> is a constant and <i>p</i> = <i>y</i> and so e* = <i>x</i>.<span
  style="mso-spacerun: yes">&nbsp; </span>We have |- (</span><span
  style='font-family:Symbol'>l </span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>p</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> <i>x</i>) : B
  </span><span style='font-family:Symbol'>�</span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> A which by
  the <i>Patterns Rule</i> is provable only if |- <i>p</i> : B and <i>p</i> : B
  |- <i>x</i> : A.<span style="mso-spacerun: yes">&nbsp; </span>But if |- <i>p</i>
  : B then <i>p</i> : B |- <i>x</i> : A iff |- <i>x</i> : A.<span
  style="mso-spacerun: yes">&nbsp; </span>Hence |- e* : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(b)
  <i>p</i> is a variable; then e* = [<i>x</i>]<i><sub>y/p</sub></i>.<span
  style="mso-spacerun: yes">&nbsp; </span>We have |- (</span><span
  style='font-family:Symbol'>l </span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>p x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>) : B </span><span
  style='font-family:Symbol'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> A which by the <i>Patterns Rule</i>
  is provable only if <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>z</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : C |- <i>z</i> : B where <i>z</i> is any arbitrary name and C is a fresh</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>fresh</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  \b </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>type variable.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>z</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : B |- [<i>x</i>]<i><sub>z/p</sub></i><sub> </sub>: A <span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Note:
  the sequent <i>z</i> : C |- <i>z</i> : B is trivially soluble by unification
  of B with the fresh</span><!--[if supportFields]><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>fresh</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  \b </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>C.<span style="mso-spacerun:
  yes">&nbsp; </span>In this case the <i>Patterns Rule</i> just acts like the <i>Abstractions
  Rule</i></span><!--[if supportFields]><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span></span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  XE &quot;<i style='mso-bidi-font-style:normal'>Abstractions Rule</i>&quot; \b
  </span><![endif]--><!--[if supportFields]><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>in Simply Typed Lambda calculus. </span><span
  style='font-size:12.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style="mso-spacerun:
  yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>But
  if <i>z</i> : B |- [<i>x</i>]<i><sub>z/p</sub></i><sub> </sub>: A for any
  arbitrary z, then certainly <i>y</i> : B |- [<i>x</i>]<i><sub>y/p</sub></i><sub>
  </sub>: A and given |- <i>y</i> : B then |- [<i>x</i>]<i><sub>y/p</sub></i><sub>
  </sub>: A and so |- e* : A. <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(c)<span
  style="mso-spacerun: yes">&nbsp; </span><i>p</i> is a pattern of the form
  (cons <i>v w</i>) or (@p <i>v w</i>); then since match(<i>p</i>, <i>y</i>) </span><span
  style='font-family:Symbol'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span><b><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>� </span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>then
  <i>match</i>(<i>p</i>, <i>y</i>) is a set </span><span style='font-family:
  Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> of bindings</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>bindings</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  \b </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp; </span>Each element &lt;<i>v</i>, <i>b</i>&gt;
  of </span><span style='font-family:Symbol'>s</span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> is an
  association of a variable <i>v</i> with a value</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>value</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  \b </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span><i>b</i>.<span style="mso-spacerun:
  yes">&nbsp; </span>We know from the <i>Patterns Rule</i></span><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;</span></i><i style='mso-bidi-font-style:normal'><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>Patterns Rule</span></i><i style='mso-bidi-font-style:
  normal'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&quot; </span></i><![endif]--><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>that (</span><span style='font-family:
  Symbol'>l </span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>p</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> <i>x</i>) : B
  </span><span style='font-family:Symbol'>�</span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> A is provable
  only if <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:1.0in;text-align:justify;text-indent:
  -.25in;mso-list:l1 level1 lfo4;tab-stops:list .5in'><![if !supportLists]>1.<span
  style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  </span><![endif]><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>1.</span><span style='font-size:7.0pt'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  </span><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>N1 </span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-style:italic'>: A1<i>,&#8230;Nn
  </i></span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'><span style="mso-spacerun: yes">&nbsp;</span>: An |- <i>p*</i>
  : B; <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:1.0in;text-indent:-.25in;mso-list:l1 level1 lfo4;
  tab-stops:list .5in'><![if !supportLists]>2.<span style='font:7.0pt "Times New Roman"'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  </span><![endif]><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>2.</span><span style='font-size:7.0pt'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  </span><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>p*</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> : B |- <i>x</i>*<sub> </sub>: A; <span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>where
  <i>N1,&#8230;Nn</i> are fresh</span><!--[if supportFields]><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>fresh</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  \b </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>names and A1,&#8230;,An are fresh type
  variables, <i>p</i>* results from <i>p</i> by replacing all the variables <i>x1,..,xn</i>
  in <i>p</i> by <i>N1</i>,&#8230;,<i>Nn</i> and x* results from x by replacing all
  the free variables from <i>x1,..,xn</i> by <i>N1</i>,&#8230;,<i>Nn</i>.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>p*</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : B |- <i>x</i>*<sub> </sub>: A<span style="mso-spacerun: yes">&nbsp;
  </span>states that assuming an arbitrary substitution instance of the
  variables in <i>p</i> (i.e. <i>p</i>*) to be of type B, that same
  substitution applied to the free</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>free</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>variables in <i>x</i> produces an
  object (i.e. <i>x</i>*) that can be proved to be of type A.<span
  style="mso-spacerun: yes">&nbsp;&nbsp; </span>Since <i>match</i>(<i>p</i>, <i>y</i>)
  succeeds <i>y</i> is a substitution instance of <i>p</i>.<span
  style="mso-spacerun: yes">&nbsp; </span>So we have<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:Symbol'>s</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(<i>p</i>)
  : B |- </span><span style='font-family:Symbol'>s</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(<i>x</i>)
  : A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>But </span><span style='font-family:
  Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(<i>p</i>) = <i>y</i> and </span><span style='font-family:
  Symbol'>s</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>(<i>x</i>) = e*.<span style="mso-spacerun: yes">&nbsp;
  </span>So we have<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>y</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> : B |- e* : A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>But
  given |- <i>y</i> : B then |- e* : A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #5; then e = (if <i>x y z</i>); and e* = <i>y</i> or e* = <i>z</i> or e*
  = </span><span style='font-family:Symbol'>^. </span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>Assume that |- e : A, then this is
  provable by the <i>Conditional Rule</i></span><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span></span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  XE &quot;Conditional Rule&quot; \b </span><![endif]--><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>and so |- <i>y</i> : A and |- <i>z</i>
  : A. Since |- </span><span style='font-family:Symbol'>^</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : A, then |- e* : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span><u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>By rule #6; then e = (let <i>x y z</i>),
  suppose |- e : A.<span style="mso-spacerun: yes">&nbsp; </span>Then by the <i>Local
  Rule</i></span><!--[if supportFields]><i style='mso-bidi-font-style:normal'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span></i><i
  style='mso-bidi-font-style:normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>Let Rule</span></i><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; </span></i><![endif]--><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>for some B, where <i>x</i>* is fresh</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>fresh</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  \b </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoFootnoteText style='margin-left:.5in'><span style='font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>|-
  <i>y</i> : B and <i>x</i>* : B |- <i>z<sub>x*/x</sub></i> : A</span></p>
  <u3:p></u3:p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Here
  e* = ((</span><span style='font-family:Symbol'>l</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  <i>x z</i>) <i>y</i>); by the <i>Applications Rule</i></span><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE &quot;<i
  style='mso-bidi-font-style:normal'>Applications Rule</i>&quot; \b </span><![endif]--><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>e* : A if for some B;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoFootnoteText style='margin-left:.5in'><span style='font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>|-
  <i>y</i> : B and <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>|- (</span><span style='font-family:
  Symbol'>l</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'> <i>x z</i>) : (B </span><span style='font-family:Symbol'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  A)<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>By the <i>Patterns Rule</i>, |- (</span><span
  style='font-family:Symbol'>l</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> <i>x z</i>) : (B </span><span
  style='font-family:Symbol'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> A) just when, where <i>x</i>* is
  fresh</span><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-begin'></span>
  XE &quot;</span><b style='mso-bidi-font-weight:normal'><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>fresh</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&quot; \b </span><![endif]--><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>and C is a fresh type variable.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>* : C |- <i>x</i>*
  : B and<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>* : B |- <i>z<sub>x*/x</sub></i>
  : A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Since
  <i>x</i> is a variable the first sequent is easily soluble (unify C with B).
  So |- e* : A if both the following are provable.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoFootnoteText style='margin-left:.5in'><span style='font-size:
  10.0pt;font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>|-
  <i>y</i> : B and <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>* : B |- <i>z<sub>x*/x</sub></i>
  : A<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-style:italic'>By
  hypothesis these are both provable, hence </span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>|- e* : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #7; then e =<span style="mso-spacerun: yes">&nbsp; </span>(cons <i>x</i>
  <i>y</i>) and |- e : A and either e* = </span><span style='font-family:Symbol'>^</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  or e* = (cons </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>x</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>y</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>).<span
  style="mso-spacerun: yes">&nbsp; </span>If e* = </span><span
  style='font-family:Symbol'>^</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> then |- e* : A.<span
  style="mso-spacerun: yes">&nbsp; </span>Suppose e* = (cons </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>y</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>).
  We write &#8216;e </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><i><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>n</span></sub></i><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'> </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e*&#8217;
  when e can be normalised to e* using <i>n</i> rewrite rules.<span
  style="mso-spacerun: yes">&nbsp; </span>The proof of subject reduction is by
  induction on <i>n</i>. Suppose <i>n</i> = 0; then e = e* and the proof is
  immediate.<span style="mso-spacerun: yes">&nbsp; </span>Suppose that subject
  reduction holds when <i>n</i> rules are used; i.e. we assume if |- e : A and
  e </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>n</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  e</span><i><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>n</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  then |- e</span><i><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>n</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : A as an inductive hypothesis.<span style="mso-spacerun: yes">&nbsp;
  </span>We wish to show |- e : A and e </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>n+1</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  e</span><i><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>n+1`</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  then |- e</span><i><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>n+1</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : A. In this case we need to show only that each individual rule of our
  semantics preserves subject reduction where no further normalisation is
  needed above what is performed in the rule itself. Such a proof is
  essentially nothing more than a reiteration of the cases already cited.<span
  style="mso-spacerun: yes">&nbsp; </span>In the case of rule #7, if no
  normalisation of <i>x</i> or <i>y</i> is required, then again e = e* and the
  proof is immediate.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>What
  our reasoning establishes is that the presence of the </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>� </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>symbol
  is irrelevant to the subject reduction property.<span style="mso-spacerun:
  yes">&nbsp; </span>Provided <i>every</i> rule preserves subject reduction in <i>every</i>
  case where no further normalisation is needed above what is performed in the
  rule itself, then subject reduction will obtain for the system overall.<span
  style="mso-spacerun: yes">&nbsp; </span>In future we will invoke this
  argument to banish the </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>� </span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>by the phrase &#8220;by induction on the
  order of rewriting&#8221;.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #8; then e =<span style="mso-spacerun: yes">&nbsp; </span>(@p <i>x</i> <i>y</i>)
  and |- e : A and either e* = </span><span style='font-family:Symbol'>^</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  or e* = (@p </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>x</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>y</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>).<span
  style="mso-spacerun: yes">&nbsp; </span>By induction on the order of
  rewriting, we drop the </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> and consider only e* = </span><span
  style='font-family:Symbol'>^</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> or e* = (@p <i>x</i> <i>y</i>).<span
  style="mso-spacerun: yes">&nbsp; </span>If e* = </span><span
  style='font-family:Symbol'>^</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> then |- e* : A.<span
  style="mso-spacerun: yes">&nbsp; </span>If e* = (@p <i>x</i> <i>y</i>) then
  the proof is immediate.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #9; then e = (++ <i>x</i>) and |- e : number.<span style="mso-spacerun:
  yes">&nbsp; </span>Either e* = </span><span style='font-family:Symbol'>^ </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>or
  e* = (1 + </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>x</span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>). If e* = </span><span
  style='font-family:Symbol'>^ </span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>then certainly |- e : number.<span
  style="mso-spacerun: yes">&nbsp;&nbsp; </span>If<span style="mso-spacerun:
  yes">&nbsp; </span></span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> is a number
  then 1 + </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>x </span></i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>is a number and by the <i>Primitive
  Rule</i>, |- 1 + </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> : number and
  so |- e* : number.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #10; then e = (- - <i>x</i>) and |- e : number.<span
  style="mso-spacerun: yes">&nbsp; </span>Either e* = </span><span
  style='font-family:Symbol'>^ </span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>or e* = (</span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x
  </span></i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>- 1). If e* = </span><span style='font-family:Symbol'>^ </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>then
  certainly |- e : number.<span style="mso-spacerun: yes">&nbsp;&nbsp;
  </span>If<span style="mso-spacerun: yes">&nbsp; </span></span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  is a number then </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> - 1<i> </i>is
  a number and by the <i>Primitive Rule</i>, |- </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  - 1 : number and so |- e* : number.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-layout-grid-align:
  none;text-autospace:none'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>By rule #11; then e = (cases <i>x</i><sub>1</sub>
  &#8230; <i>x<sub>n</sub></i>) and |- e : A. Either </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-bidi-font-style:italic'>1</span></sub><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>= </span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  or </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-bidi-font-style:italic'>1</span></sub><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> </span></i><span style='mso-bidi-font-size:
  12.0pt;font-family:Symbol'>� </span><b><span lang=EN-GB style='font-family:
  Symbol;mso-ansi-language:EN-GB'>�</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>.<span style="mso-spacerun:
  yes">&nbsp; </span>By induction on the order of rewriting, we drop the </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  and consider only the cases <i>x</i><sub><span style='mso-bidi-font-style:
  italic'>1</span></sub><i> </i>= </span><b><span lang=EN-GB style='font-family:
  Symbol;mso-ansi-language:EN-GB'>�</span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> or not <i>x</i><sub><span
  style='mso-bidi-font-style:italic'>1</span></sub><i> </i>= </span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�. <u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-layout-grid-align:
  none;text-autospace:none'><b><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-layout-grid-align:
  none;text-autospace:none'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>If <i>x</i><sub><span
  style='mso-bidi-font-style:italic'>1</span></sub><i> </i>= </span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  then e* = (cases &#8230; <i>x<sub>n</sub></i>).<span style="mso-spacerun:
  yes">&nbsp; </span>By the <i>Cases Rule</i></span><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE
  &quot;Cases Rule&quot; \b </span><![endif]--><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  |- e : A just when each <i>x<sub>i</sub></i> in (cases <i>x</i><sub>1</sub> &#8230;
  <i>x<sub>n</sub></i>) is such that |- <i>x<sub>i</sub></i> : A.<span
  style="mso-spacerun: yes">&nbsp; </span>So certainly it must be true that |-
  (cases &#8230; <i>x<sub>n</sub></i>) : A and therefore |- e* : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>If
  <i>x</i><sub><span style='mso-bidi-font-style:italic'>1</span></sub><i> </i></span><span
  style='mso-bidi-font-size:12.0pt;font-family:Symbol'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><b><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>,
  then e* = <i>x</i><sub><span style='mso-bidi-font-style:italic'>1 </span></sub>and
  since by the <i>Cases Rule</i></span><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE &quot;Cases
  Rule&quot; \b </span><![endif]--><!--[if supportFields]><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>for each <i>x<sub>i</sub></i> in
  (cases <i>x</i><sub>1</sub> &#8230; <i>x<sub>n</sub></i>), |- <i>x<sub>i</sub></i>
  : A then |- <i>x</i><sub><span style='mso-bidi-font-style:italic'>1 </span></sub>:
  A and so |- e* : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #12; then e* = </span><b><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>� </span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-bidi-font-style:italic'>and since </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>|-
  </span><b><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : (</span><span style='font-family:Symbol'>&quot;</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  A A)), subject reduction holds.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #13; then e = (where <i>x y</i>) and e* = (if <i>x y</i> </span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>).<span
  style="mso-spacerun: yes">&nbsp; </span>Suppose |- e : A, then by the <i>Guard
  Rule</i>, |- <i>x</i> : boolean</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>boolean</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>and |- <i>y</i> : A. By the <i>Conditional
  Rule</i></span><!--[if supportFields]><i style='mso-bidi-font-style:normal'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE
  &quot;Conditional Rule&quot; \b </span><![endif]--><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span></i><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>to prove |- e* : A, it suffices to
  prove |- <i>x</i> : boolean</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>boolean</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>and |- <i>y</i> : A and |- </span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>� </span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>:
  A. By hypothesis, the first two are provable and the third follows from |- </span><b><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : (</span><span style='font-family:Symbol'>&quot;</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  A A)).<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #14; in that case e is a combinator</span><!--[if supportFields]><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style='mso-element:field-begin'></span> XE &quot;</span><b style='mso-bidi-font-weight:
  normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>combinator</span></b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&quot;
  </span><![endif]--><!--[if supportFields]><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-element:field-end'></span></span><![endif]--><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'><span
  style="mso-spacerun: yes">&nbsp;</span>expression, </span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(</span><b><i><span lang=EN-GB style='font-family:
  "Signet Roundhand";mso-ansi-language:EN-GB'>Y</span></i></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'> </span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(</span><span style='font-family:
  Symbol'>l </span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>v</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> <i>x</i>)</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>) </span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>and e* = </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>[</span><i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>]<sub>v/</sub></span><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span></sub><b><i><sub><span
  lang=EN-GB style='font-family:"Signet Roundhand";mso-ansi-language:EN-GB'>Y</span></sub></i></b><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp; </span></span></sub><sub><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(</span></sub><sub><span
  style='font-family:Symbol'>l </span></sub><i><sub><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>v</span></sub></i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  <i>x</i>)</span></sub><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>)</span></sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>.<span
  style="mso-spacerun: yes">&nbsp; </span>Assume e : A, then </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span><b><i><span lang=EN-GB
  style='font-family:"Signet Roundhand";mso-ansi-language:EN-GB'>Y</span></i></b><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> </span><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(</span><span
  style='font-family:Symbol'>l </span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>v</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> <i>x</i>)</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>)<span style="mso-spacerun:
  yes">&nbsp; </span>: A and this is provable only if </span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>v</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : A |- <i>x </i>: A.<span style="mso-spacerun: yes">&nbsp; </span>Consider
  the proof tree for <i>v</i> : A |- <i>x </i>: A.<span style="mso-spacerun:
  yes">&nbsp; </span>For every subgoal of the form <i>v</i> : A, the assumption
  <i>v</i> : A will be used to solve it.<span style="mso-spacerun:
  yes">&nbsp;&nbsp; </span>Now replace this subgoal by </span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>(</span><b><i><span lang=EN-GB style='font-family:
  "Signet Roundhand";mso-ansi-language:EN-GB'>Y</span></i></b><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'><span style="mso-spacerun: yes">&nbsp; </span></span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>(</span><span
  style='font-family:Symbol'>l </span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>v</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> <i>x</i>)</span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>) and drop the assumption </span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>v</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : A</span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>.<span
  style="mso-spacerun: yes">&nbsp; </span>By the <i>Combinator Rule</i></span><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'><span
  style='mso-element:field-begin'></span></span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> XE &quot;</span><i
  style='mso-bidi-font-style:normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>Combinator
  Rule</span></i><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>&quot; \b </span><![endif]--><!--[if supportFields]><i
  style='mso-bidi-font-style:normal'><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'><span
  style='mso-element:field-end'></span></span></i><![endif]--><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>, this is provable if </span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>v</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  : A |- <i>x </i>: A, which by hypothesis <i>is</i> provable.<span
  style="mso-spacerun: yes">&nbsp; </span>Hence if there is a proof of <i>v</i>
  : A |- <i>x </i>: A then there is a proof of </span><span lang=EN-GB
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman";
  mso-ansi-language:EN-GB'>[</span><i><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>x</span></i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>]<sub>v/</sub></span><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span></sub><b><i><sub><span
  lang=EN-GB style='font-family:"Signet Roundhand";mso-ansi-language:EN-GB'>Y</span></sub></i></b><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp; </span></span></sub><sub><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>(</span></sub><sub><span
  style='font-family:Symbol'>l </span></sub><i><sub><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>v</span></sub></i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  <i>x</i>)</span></sub><sub><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>) </span></sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>: A and so |- e* : A.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;mso-outline-level:1'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #15; in that case e is an application (<i>x y</i>). Suppose |- e : A and
  e* =<span style="mso-spacerun: yes">&nbsp; </span></span><span
  style='font-family:Symbol'>^</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> then |- e* : A.<span
  style="mso-spacerun: yes">&nbsp; </span>Suppose e* = </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'><span style="mso-spacerun:
  yes">&nbsp;</span></span><span lang=EN-GB style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman";mso-ansi-language:EN-GB'>(</span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>y</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>).<span
  style="mso-spacerun: yes">&nbsp; </span>By induction on the order of
  rewriting, we drop the </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> and consider only the case </span><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>(</span><i><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>x</span></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  <i>y</i>) and the proof is trivial.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;mso-outline-level:1'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>By
  rule #16; then e = e* and the proof is immediate.<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify;mso-outline-level:
  1'><b><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>Theorem 3: </span></b><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>if |- e : A then, if </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e
  is a p.d., then </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>e : A. <u3:p></u3:p></span></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><b><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></b></p>
  <p class=MsoNormal style='margin-left:.5in;text-align:justify'><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>Assume
  |- e : A and </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:
  EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman"'>e is a p.d.. We write &#8216;e </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'>m</span></sub></i><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'> </span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e*&#8217;
  when e can be normalised to e* using <i>m</i> rewrite rules. The proof is by
  induction on <i>m</i>. If e </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><sub><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>0</span></sub><span style='font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'> </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e,
  then e is a normal form and by theorem 1, </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e
  : A..<span style="mso-spacerun: yes">&nbsp; </span>Assume the theorem holds
  for <i>n</i> rewrites.<span style="mso-spacerun: yes">&nbsp; </span>Assume e </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>n</span></sub></i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>+1</span></sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e;
  then for some e<i>*</i>, e </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'> e<i>*</i> </span><span lang=EN-GB
  style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><sub><span
  lang=EN-GB style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:
  "Times New Roman";mso-ansi-language:EN-GB'> </span></sub><i><sub><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>n</span></sub></i><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e.<span
  style="mso-spacerun: yes">&nbsp; </span>By theorem 2 we know that if |- e : A
  then |- e* : A, and by the inductive hypothesis, we have if<span
  style="mso-spacerun: yes">&nbsp; </span>|- e* : A then </span><span
  lang=EN-GB style='font-family:Symbol;mso-ansi-language:EN-GB'>�</span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>e
  : A. So |- e : A implies </span><span lang=EN-GB style='font-family:Symbol;
  mso-ansi-language:EN-GB'>�</span><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>e : A.<u3:p></u3:p></span></p>
  <p><br clear=all style='mso-special-character:line-break'>
  </p>
  <div class=MsoNormal><span style='font-size:12.0pt'>
  <hr size=1 width="33%" align=left>
  </span></div>
  <p class=MsoFootnoteText style='text-align:justify'><a style='mso-footnote-id:
  ftn2' href="#_ftn2" name="_ftnref2" title=""><span
  class=MsoFootnoteReference><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'><span style='mso-special-character:
  footnote'><![if !supportFootnotes]>[2]<![endif]></span></span></span></a><span
  class=MsoFootnoteReference><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>[1]</span></span><span
  style='font-family:"Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>
  </span><span style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:
  "Microsoft Sans Serif";mso-bidi-font-family:"Times New Roman"'>A potential
  for confusion exists between the use of </span><span style='font-size:8.0pt;
  mso-bidi-font-size:10.0pt;font-family:Symbol'>� </span><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>for logical implication and </span><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:Symbol'>� </span><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>for the function space type
  operator.<span style="mso-spacerun: yes">&nbsp; </span>Rather than relying on
  context alone to disambiguate the intended meaning, the proof uses the older </span><span
  lang=EN-GB style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:Symbol;
  mso-ansi-language:EN-GB;layout-grid-mode:line'>� </span><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>for logical implication and </span><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:Symbol'>� </span><span
  style='font-size:8.0pt;mso-bidi-font-size:10.0pt;font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>for the type operator.<u3:p></u3:p></span></p>
  <p class=MsoFootnoteText><span style='font-family:"Microsoft Sans Serif";
  mso-bidi-font-family:"Times New Roman"'>&nbsp;<u3:p></u3:p></span></p>
  </td>
 </tr>
</table>

</div>

<p class=MsoNormal><span style='font-size:12.0pt'><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></span></p>

</div>

<div style='mso-element:footnote-list'><![if !supportFootnotes]><br clear=all>

<hr align=left size=1 width="33%">

<![endif]>

<div style='mso-element:footnote' id=ftn1>

<p class=MsoNormal><a style='mso-footnote-id:ftn1' href="#_ftnref1" name="_ftn1"
title=""></a><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></p>

</div>

<div style='mso-element:footnote' id=ftn2>

<p class=MsoNormal><a style='mso-footnote-id:ftn2' href="#_ftnref2" name="_ftn2"
title=""></a><![if !supportEmptyParas]>&nbsp;<![endif]><o:p></o:p></p>

</div>

</div>

</body>

</html>
